Computer programs and software are ubiquitous and are used not just to direct the functionality of conventional computers but also to control and enhance the functionality of a myriad of modern products and appliances. For instance, televisions, household appliances, cellular phones, automobiles, medical devices, and so forth, may incorporate computer programs which direct and enhance their functionality. The theoretical and practical analysis of computer programs is an important aspect of software research, development, modification, enhancement, and maintenance. The ability to analyze computer programs and reason about their execution, from both theoretical and practical perspectives, aids software developers by allowing them to make better and more informed choices during development of software and the modification or enhancement of existing software. Analysis of software is useful for proving correctness of code, for performing optimizations of existing code, for doing performance analysis and so on.
For purposes of analysis, it is often efficient and desirable to automate the reasoning about the complexity of software using tools and abstractions which can describe the properties and behavior of computer software. Computer software may often be formally described for the purposes of such analysis by specifying a set of constraints or axioms formalizing the relationships and operation of the software.
Satisfiability Modulo Theories (SMT) is the problem of solving constraints in a combination of domains. Typical domains include linear arithmetic over real numbers and integer linear arithmetic over the integers. Linear programming as exemplified by the well-known Simplex algorithm is a prime example of a solver for Linear arithmetic. A satisfiability (SAT) solver is a procedure that determines satisfiability of propositional formulas.
It may also be useful to reason at the same time about disparate sets of constraints and axioms. Modern theory provers (constraint solvers) have been used in such pursuits. A core problem of Satisfiability Modulo Theories is combining separate theory solvers for a plurality of theories into a combined solver for the union. The manifestation of the problem for a pair of theories T1 and T2, is to produce a combined solver for the union T1∪T2. One may appreciate that a pairwise combination method that works indepdently of the theories may produce an n-way combination method by repeated pairing. The Nelson-Oppen combination method identifies sufficient conditions for combining two theories over disjoint signatures: only (disjunctions of) equalities over shared variables that are implied by one of the theories need to be communicated to the other solver.
Some traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals into the search space. Many existing implementations and optimizations of these methods seek to efficiently implement the trigger:
if Ti∪Γi′u≃v then propagate u≃v,
to exhaustively enumerate all implied (disjunctions of) equalities for a theory Ti and constraints Γi that are asserted in its context.
Another known method to obtain completeness is by enumerating equalities corresponding to the cross-product of all shared variable pairs and use a SAT solver for non-deterministically choosing a partition based on the cross-product. Common to these methods is that they are pessimistic about which equalities are propagated.
Methods for combining theories and solving the combined theories are known to consume both large amounts of computing resources (space and processor power) as well as time. There can be considerable overhead in space and in expensive theory propagation required by these methods.